Nuprl Lemma : length-append
11,40
postcript
pdf
as
,
bs
:(top List). sqequal(||append(
as
;
bs
)||; (||
as
|| + ||
bs
||))
latex
Definitions
||
as
||
,
x
:
A
.
B
(
x
)
,
top
,
t
T
Lemmas
top
wf
,
length
wf1
origin
as,bs:(top List). sqequal(||append(as; bs)||; (||as|| + ||bs||)) as,bs:(top List). sqequal(||append(as; bs)||; (||as|| + ||bs||)) x:A. B(x)
T